V = 4

Below is a failure‑seeking review of PSP‑1 with concrete edits. I’ve grouped feedback into: (A) critical inconsistencies and correctness bugs, (B) structural/style changes to make this feel like an RFC/EIP/BIP‑grade spec, (C) oversights and attack surfaces you haven’t addressed, and (D) a clean, regularized ToC plus redlines you can drop in.

I cite relevant public standards where it helps readers triangulate (RFC2119/8174 language, TLS exporters, DPoP, CBOR/COSE, JCS, DSSE, CIDs, Biscuit). I also tie back to your internal docs (Receipt Rails, TAP/RAM, CEP/BA placement) where PSP‑1 leans on those concepts. ([RFC Editor]1) Internals: receipts are enforcer‑minted (PoAR), acceptance is TAP/RAM, BA/CEP vocabulary and placement, etc.

A) Critical inconsistencies & correctness bugs (will break interop)

1. Atoms, Symbols, and Variables appear, then are forbidden.

   • Where: Terminology says Literals are “Atoms or pure, bounded Builtins” and Terms include Sym/…/Var; the Language Model later says “builtin literals only; … No variables. No user‑defined atoms.” PCF sorting mentions “Builtin before Atom if Atoms are present.”
   • Why this fails: You can’t both ban and accommodate Atoms/Vars. Canonicalization rules also rely on a literal kind that shouldn’t exist.
   • Edit: Delete Atom/Sym/Var from PSP‑1. Say “CPL/0 literals are Builtins only; Terms ∈ {Str, Int, Bool, Bytes}.” Remove the PCF bullet mentioning Atom. Update Appendix A grammar accordingly (see Section D).

2. Interval boundaries are inconsistent.

   • Where: Algorithm uses now >= iat AND now < exp for Presentation lifetime. Builtin within_time(now, nbf, exp) says true iff nbf <= now <= exp. ttl_ok uses now <= iat + ttl_max.
   • Why this fails: Inclusive vs half‑open windows will produce different “pass/fail” near edges.
   • Edit: Pick one convention across the spec. Recommendation: half‑open windows [nbf, exp), which is what many IETF/JOSE flows use for expiries. State this once in “Time Model & Boundaries.” Align within_time and default Presentation/Grant window checks with half‑open. Cite RFC 7519’s common usage and BCP‑style guidance. ([RFC Editor]2)

3. Ambiguity in attenuation w.r.t. Checks and Queries.

   • Where: You say “child MAY add Checks; MUST NOT remove any parent Check that controls authority”, and “For any retained parent Query, child Literals ⊇ parent Literals; child MAY add Literals.” You also imply a child may drop Queries (since OR‑removal narrows).

   • Why this fails: “controls authority” is subjective and unverifiable; implementers can’t agree on what counts as “controlling.”

   • Edit: Make the rule syntactic and total:

     • Checks: child MUST include at least the parent’s full set of Checks (by identity after PCF). It MAY add Checks.
     • Queries (inside each Check): child MAY drop any subset of parent Queries (narrowing the OR), or keep and tighten them. For any retained Query, the child’s literal multiset MUST be a superset (constants tightened per builtin rules).
     • Literal constants: only tighten as defined in the Builtins registry.
       This exactly matches the “checks‑only attenuation” pattern in Biscuit (append checks; never remove constraints), which readers will recognize. ([Eclipse Biscuit]3)

4. TTL semantics are underspecified vs. exp.

   • Where: You say exp - iat SHOULD be short and separately use ttl_ok(iat, now, ttl_max).
   • Why this fails: An implementation could pass ttl_ok while now >= exp denies, or vice‑versa.
   • Edit: Define precedence: the effective Presentation lifetime is ([iat, exp) ∩ ttl_ok). Specify that both must pass; if exp is present, exp - iat SHOULD also be ≤ ttl_max (if both are used), else deny. Tie explicitly to the single captured now. See RSA of JWT exp/iat and JWT BCP for edge guidance. ([RFC Editor]2)

5. Comparator drift risk across time without pinning.

   • Where: You pin builtins and (if used) the channel lattice, but you do not pin scheme comparator versions; you only select by scheme name.
   • Why this fails: If a scheme’s normalization or subset comparator evolves, two CEPs may render different decisions for the same Grant over time. “Deny on unknown” doesn’t help if semantics change silently.
   • Edit: Either (a) pin a schemes_snapshot_id (a content‑addressed manifest enumerating each scheme name → comparator_id), or (b) require a PoAR to record the comparator fingerprint(s) used at enforcement for audit. I recommend (a) for strict determinism. Use CID/multihash for the manifest. ([GitHub]4)

6. Channel binding profile naming not tied to IETF registries.

   • Where: You reference TLS exporter and DPoP but don’t name the binding exactly or cite specs.

   • Why this fails: Interop will break if “tls_exporter:v1” isn’t clearly defined relative to TLS 1.3’s exporter binding and its registry.

   • Edit: Define the profile strings and cite the standards:

     • tls-exporter per TLS 1.3 + RFC 9266 (“tls‑exporter” channel binding for TLS 1.3), derived from RFC 5705/8446.
     • dpop per RFC 9449.
       Require channel_lattice_id to enumerate these profile identifiers unambiguously. ([RFC Editor]5)

7. PCF mentions encodings and kinds you forbid elsewhere.

   • Where: PCF has rules about “indefinite‑length encodings” and “Atoms.”
   • Edit: Keep PCF language entirely format‑agnostic; put all on‑wire determinism in PSP‑3 (CBOR Canonical/Deterministic per RFC 8949 + COSE 9052 or JCS 8785 for JSON‑style encodings; DSSE if you want envelope neutrality). Only define the abstract sort/ordering in PSP‑1. ([IETF Datatracker]6)

8. Environment fact normalization is partially specified.

   • Where: You require resources to be normalized via scheme comparators, and strings to be NFC, but you don’t state when normalization occurs for env facts.
   • Edit: Require CEPs to normalize input facts—especially resource—before evaluation, using the same comparator semantics as declaration canonicalization, or deny. (You already hint at this; promote it to a single, normative rule in “Evaluation Environment”.)

9. Grant/Presentation cross‑references to TAP/RAM/Receipts are scattered and sometimes conflicting.

   • Where: PSP‑1 claims receipts and acceptance live elsewhere (PSP‑2/TAP), while examples and the algorithm dictate PoAR behavior and denial reason codes.
   • Edit: Move all receipt‑field specifics and reason‑code registries to PSP‑2 and reference them normatively from PSP‑1. The “enforcer mints the proof” invariant and receipt placement (P/R/S) should remain in PSP‑1 as a short invariant and a pointer (your Receipt Rails docs align with this).

10. Terminology collision around CEP/BA roles and acceptance.

• Where: PSP‑1 mentions “CEP/BA spec,” anchoring, acceptance/TAP. Your architecture docs already standardize CEP(R)/CEP(P)/CEP(S), BA subtypes, exposure modes, and acceptance responsibilities.
• Edit: Add a normative terminology subsection with that vocabulary and a stable reference to the CEP/BA placement profile: CEP(R), CEP(P), CEP(S)/SSA; BA is a CEP subtype that bridges non‑native SoA via long‑lived leases; exposure modes mediate/derive/reveal with TAP policy defaults.

B) Structural & style changes (clean, RFC/EIP/BIP‑grade)

B1. “Requirements Language” paragraph
Keep the BCP14 boilerplate exactly per RFC 8174 and 2119 (you already have it, good). Ensure it appears early and applies by default; avoid sprinkling “(normative)” all over. ([RFC Editor]7)

B2. Normalize section headings across all ##
Adopt an RFC/EIP‑like rhythm so each major section is familiar to implementers and reviewers:

1.  Abstract
2.  Terminology and Requirements Language
3.  Overview (goals/non-goals, threat model pointers)
4.  Capability Program (CPL/0)
    4.1 Language Model (structure, monotonicity)
    4.2 Types and Terms
    4.3 Builtins (registry-pinned)
    4.4 Evaluation Environment (facts, normalization)
    4.5 Declarations (PairSet, ActionSet, ResourceSet)
    4.6 Attenuation Semantics
5.  Semantic Pinning
6.  Program Canonical Form (PCF)
7.  Grants
8.  Presentations
9.  Delegation and Attenuation (chain verification)
10. Revocation and Rotation
11. CEP Verification Algorithm (stepwise)
12. Security Considerations
13. IANA / Registry Considerations (if you’ll register op_ids)
14. Test Vectors and Interop
15. References
Appendix A: CPL/0 Grammar (structure-only)
Appendix B: Builtins and Tightening Rules
Appendix C: Scheme Comparator Requirements

B3. Move all on‑wire concerns to PSP‑3.
In PSP‑1, keep PCF purely abstract. In PSP‑3, point to deterministic encodings (CBOR canonical form per RFC 8949 + COSE 9052, or JSON + JCS RFC 8785 + JWS 7515/DSSE). State a single rule: identity = multihash(CanonicalBytes) with algorithm parameters pinned. ([IETF Datatracker]6)

B4. Reference EIP/BIP editorial expectations.
Include short “Rationale”, “Security Considerations”, and “Test Vectors” sections—EIP‑1 explicitly lists them, and reviewers expect them. ([Ethereum Improvement Proposals]8)

B5. Remove “(normative)” clutter.
Make entire sections normative by default; label diverging parts “Informative” in headings.

C) Oversights & attack surfaces (things you haven’t considered enough)

1. Comparator set pinning & drift (already called out). Without it, a later update to vault: or k8s: normalization can silently flip allow/deny; audits become non‑replayable. Pin a schemes_snapshot_id or record comparator fingerprints in PoARs. ([GitHub]4)

2. Channel binding registry & floor semantics. Name the exact RFC bindings and ensure your channel_lattice_id snapshot enumerates them with partial order comparisons. Example elements: mtls:v1, tls-exporter:v1, dpop:v1, bearer:v1. Use RFC 9266 for TLS 1.3 exporter binding and RFC 9449 for DPoP. ([RFC Editor]5)

3. Replay & binding collisions. Spell out nonces (jti) and one‑time use or maxUses in builtins (tightening rule must be monotone). Clarify how channel profile strings map to RFCs (above) to prevent weak aliasing.

4. Resource explosion / selector bounds. You forbid unbounded globs/regex but permit “bounded prefixes.” Add explicit size/complexity limits on declaration sets and selector forms (max entries, max total bytes) and require CEPs to enforce resource budgets (you partly do; make it crisp).

5. Time discipline and skew. You defer to TAP; add a one‑liner: CEP MUST capture a single now and apply TAP’s skew policy consistently to all checks (within_time, envelope windows, ttl_ok), then cite that in the algorithm (you already do; make it top‑level invariant).

6. Reveal mode implications. PSP‑1 notes reveal is high risk; point to TAP language requiring strict penalties or forbidding for high‑assurance profiles and require PoAR to mark exposureMode=reveal. Your internal docs already argue this and define break‑glass receipts. Link it.

7. Lease freshness verification inputs. Specify the environment fact (lease_status) and ban network I/O in builtins; say how a CEP checks lease freshness: only via TAP‑approved, locally available attestations. (You imply this; make it explicit.)

8. Attestation of runtime (enforcer identity & version). Receipts and audits will need enforcer measurement (adapterRef/build attestation) recorded in PoAR for traceability (you have this in Receipt Rails; link from PSP‑1 to PSP‑2/TAP).

9. Test vectors & conformance suite. Add a dedicated section with cross‑platform test vectors for:

   • PCF identity stability (different literal orders collapse to the same program_id)
   • Attenuation proofs (valid/invalid child examples)
   • Boundary time cases (nbf/exp edges)
   • Comparator normalization (tricky URIs, percent‑encoding)
     EIP‑style specs always ship tests. ([Ethereum Improvement Proposals]8)

10. Reference to an external logic (Biscuit) must be precise. You map CPL/0 to Biscuit checks; offer a normative equivalence only for the checks‑only fragment and ban variables/rules. Cite the Biscuit spec page(s) rather than blog posts. ([Eclipse Biscuit]3)

D) Drop‑in redlines (tightening language; safe defaults)

Replace “Literals and Terms” in Language Model with:
Literals are invocations of pure, deterministic, bounded Builtins. CPL/0 does not have user‑defined atoms, variables, rules, recursion, or negation. Terms are ground and typed: Str, Int (arbitrary‑precision), Bool, Bytes.

Replace the attenuation bullets in “Attenuation by Derivation” with:
Program checks: The child MUST include all parent checks (by PCF identity) and MAY add additional checks.
Queries per check: For any retained parent Query, the child query’s literal multiset MUST be a superset; the child MAY drop any subset of the parent’s queries (narrowing).
Literal constants: Constants MUST only tighten according to the builtin’s tightening rule in the pinned builtins_id (e.g., narrower time window; lesser or equal TTL; higher or equal channel floor).
Declarations: Each child declaration MUST be a subset of the corresponding parent declaration under the same normalization/comparator semantics.

Replace the time semantics with a single “Time Model & Boundaries” clause:
The CEP captures a single logical now at enforcement start. Unless otherwise specified, all time windows are half‑open [start, end). Presentation lifetime is enforced as: now ∈ [iat, exp) AND any ttl_ok constraint; if both exp and ttl_ok are present, both MUST pass. Failures MUST deny. ([RFC Editor]2)

In “Evaluation Environment,” add:
The CEP MUST normalize resource using the same scheme comparator semantics used to canonicalize declarations before evaluation. Normalization failure MUST deny.

In “Semantic Pinning,” add:
schemes_snapshot_id (RECOMMENDED): a content‑addressed manifest pinning the exact comparator entry for each scheme name referenced by declarations. If absent, CEPs MUST record comparator fingerprints in receipts (PSP‑2). Unknown or mismatched comparator versions across delegation hops MUST deny. ([GitHub]4)

In “Builtins and registries,” add explicit profile examples and citations:
channel_geq(channel, floor) compares profiles (e.g., mtls:v1, tls-exporter:v1, dpop:v1, bearer:v1) under the pinned lattice. tls-exporter:v1 corresponds to the TLS 1.3 exporter channel binding (RFC 9266); dpop:v1 corresponds to RFC 9449 DPoP; bearer:v1 represents no sender‑constraining. ([RFC Editor]5)

In Appendix A – CDDL grammar:
Remove Sym/Var, enforce Literal = { op: tstr, args: [* Term] } with Term = Str / Int / Bool / Bytes only. Make clear: structure only; on‑wire encodings are in PSP‑3.

In “Frame and Canonical Bytes”:
Keep only the abstract identity rule in PSP‑1. Move CBOR/COSE (RFC 8949/9052), JSON/JCS (RFC 8785), DSSE envelope decisions to PSP‑3. If you want JOSE compatibility, cite JWS 7515 and JWT 7519 as profiles (optional). ([IETF Datatracker]6)

In “Security Considerations” add acceptance hooks instead of details:
Receipt emission (PoAR), deny reasons, exposure mode penalties, lease freshness, and adapter measurement (e.g., adapterRef) are defined in PSP‑2 and TAP. PSP‑1 mandates that the enforcer mint an Access PoAR on success or a DenyReceipt on failure (placement per CEP(R/P/S) profile). See Receipt Rails.

E) Smaller editorial tightening (high ROI)

• Delete repeated “normative” markers. Use “Informative” only where needed.
• Use consistent field casing in examples (channelBinding vs channel_binding). Since PSP‑1 doesn’t define on‑wire names, keep examples consistent in one style and remind readers the names are illustrative.
• Consolidate “Non‑goals.” Move enforcement placement, transport, receipts, and governance pointers into a single “Out of Scope & References” section with precise forward references (PSP‑2/‑3, TAP).
• Reason codes: Declare they live in PSP‑2 (Receipt rails), not here. Your internal doc already enumerates them and shows where PoAR is minted.

F) Things to add (short subsections)

1. Threat model pointers. A 1‑page “threats we explicitly handle” (replay, token theft, comparator drift, clock skew, authority broadening) and “out of scope” (network I/O in evaluation, ZK proofs).
2. IANA/Registry considerations. If you ever want to register builtin op‑ids or channel profiles, reserve a section stub now.
3. Test vectors. Provide three complete, executable examples per domain with canonical bytes, program_id, and declaration CIDs.
4. Interoperability with Biscuit. Define the canonical transformation for the checks‑only fragment (strict mapping rules). ([Eclipse Biscuit]3)

G) Consistency with your surrounding documents

• Receipts & acceptance — PSP‑1 should rely on PSP‑2/TAP for PoAR/VOR/Views, reason codes, and acceptance thresholds. Your Receipt Rails doc already fixes the invariant that the enforcer mints the proof and shows placement variants. Cross‑reference rather than restating fields.
• CEP vs BA vocabulary — your TrustOS architecture docs define CEP(R/P/S), BA as a subtype, SSA terminology, and exposure modes; incorporate that vocabulary once and reuse.
• Reveal penalties & break‑glass receipts — call them out in Security Considerations and point to TAP constraints and Receipt Rails (BreakGlassReceipt).

H) Example micro‑diffs (ready to paste)

H1. Language Model — Literals/Terms

Before:
Uses builtin literals only: Builtin(op_id, [arg...]). Terms are ground: Str | Int | Bool | Bytes. No variables. No user‑defined atoms.
After:
Literals are builtin invocations: Builtin(op_id, [arg...]). CPL/0 has no user‑defined predicates, atoms, variables, rules, or recursion. Terms are ground and typed: Str | Int | Bool | Bytes.

H2. PCF — remove Atom, keep abstract

Before:
literal kind (e.g., Builtin before Atom if Atoms are present)
After:
sort literals by (operator id, arguments under canonical term order). CPL/0 defines only builtin literals.

H3. Attenuation

Before:
A child Program MAY add Checks; it MUST NOT remove any parent Check that controls authority…
After:
A child MUST include all parent Checks (by PCF identity) and MAY add Checks. Within each retained parent Query, the child literal multiset MUST be a superset; the child MAY drop queries (narrow the OR). Literal constants MUST only tighten per builtin rules.

H4. Time model

CEPs capture a single now. All windows are [start, end). Presentation acceptance requires now ∈ [iat, exp) and all time‑related builtins (e.g., ttl_ok) to pass; if both exp and ttl_ok are present, both MUST pass.

H5. Semantic pinning

Add schemes_snapshot_id (content‑addressed manifest) to the Grant pins. In a delegation chain the child’s schemes_snapshot_id MUST equal the parent’s.

I) Quick checklist for final pass (editorial QA)

• Remove Atom/Sym/Var everywhere; update Appendix A grammar.
• Align time boundaries to half‑open and state precedence of exp and ttl_ok.
• Replace “controls authority” wording with the syntactic MUSTs above.
• Introduce schemes_snapshot_id or require comparator fingerprints in PoAR.
• Define channel binding profiles with RFC citations (9266, 9449) and pin via channel_lattice_id.
• Move on‑wire specifics to PSP‑3 (CBOR/COSE, JCS/JWS/DSSE).
• Point all receipt fields and reason codes to PSP‑2 and TAP/RAM.
• Add a Test Vectors section.
• Normalize capitalization/field casing across examples.

Sources (selected)

• Requirements language (BCP14): RFC 2119; RFC 8174. ([RFC Editor]1)
• TLS exporters & channel binding: RFC 8446 (TLS 1.3); RFC 9266 (tls‑exporter for TLS 1.3); RFC 5705 (KM exporters). ([RFC Editor]9)
• DPoP sender‑constraining: RFC 9449. ([RFC Editor]10)
• Canonical encodings & envelopes: RFC 8949 (CBOR); RFC 9052 (COSE); RFC 8785 (JCS); RFC 7515 (JWS); DSSE spec. ([IETF Datatracker]6)
• CIDs/multihash for content addressing: Multiformats CID spec; IPFS docs. ([GitHub]4)
• Biscuit checks‑only mapping: Biscuit specifications & docs. ([Eclipse Biscuit]3)
• Receipt Rails & acceptance (internal alignment): enforcer‑minted PoAR, deny receipts, TAP/RAM, CEP/BA placement vocab.

If you want, I can produce a cleaned “PSP‑1 (Editor’s Cut)” markdown that (1) applies the redlines above, (2) removes duplication and “(normative)” noise, (3) adds a one‑page time model, and (4) stubs test vectors.